T:Type, l1, l2, l3:(T List). l1  l2 @ l3  (||l1||  ||l2||)  l1  l2 

latex

Definitions	l1  l2, t  T, P  Q, x:A. B(x), P  Q, P & Q, P  Q, x:A. B(x), False, A, A  B, P  Q, as @ bs, ||as||
Lemmas	le wf, iseg wf, append wf, iseg append iff, length wf1, length append